-
Notifications
You must be signed in to change notification settings - Fork 1k
feat(Order): order types #34034
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
feat(Order): order types #34034
Conversation
PR summary 721b21cf2bImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
OrderTypes definitionsOrderType definitions
🚨 PR Title Needs FormattingPlease update the title to match our commit style conventions. Errors from script: Details on the required title formatThe title should fit the following format:
|
OrderType definitionsOrderType definitions
OrderType definitionsOrderType definitions
Co-authored-by: Violeta Hernández Palacios <[email protected]>
Co-authored-by: Violeta Hernández Palacios <[email protected]>
|
This PR/issue depends on: |
Even though it is local and not exposed
OrderType definitions|
-awaiting-author |
| ⟨⟨h⟩,hne⟩ | ||
| ⟨⟨h⟩, hne⟩ | ||
|
|
||
| alias _root_.OrderEmbedding.type_le_type := type_le_type |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't this be?
| alias _root_.OrderEmbedding.type_le_type := type_le_type | |
| alias _root_.OrderEmbedding.orderTypeType_le_orderTypeType := type_le_type |
I do find this name extremely clunky. Perhaps we can stretch the naming conventions just a bit?
| alias _root_.OrderEmbedding.type_le_type := type_le_type | |
| alias _root_.OrderEmbedding.orderType_le_orderType := type_le_type |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The current name is okay if we believe that type here unambiguously refers to OrderType.type, which... I could believe?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There's also Ordinal.type.
Co-authored-by: Violeta Hernández Palacios <[email protected]>
Co-authored-by: Violeta Hernández Palacios <[email protected]>
Adding the basic definitions around order types, the equivalence classes of linear orders under order isomorphism.
See draft discussion at #33420 and refactoring task #28278 .
OrderIsoinvolvingProdandLex#33663LinearOrderinstance forEmpty#31889